EXECUTED_PROGRAM

ret > ExitSuccess
out > Word.NumWord =
out >   Agda.Builtin.FromNat.Number.constructor _ (λ a _ → toWord64 a)
out > Word.NumNat = Agda.Builtin.FromNat.Number.constructor _ (λ a _ → a)
out > Word.natOp = λ a b c → toWord64 (a (fromWord64 b) (fromWord64 c))
out > Word._^_ =
out >   λ a b →
out >     case b of
out >       0 → 1
out >       _ → let c = b - 1 in a * Word._^_ a c
out > Word.2⁶⁴ = Word._^_ 2 64
out > Word.addWord = λ a b → a +64 b
out > Word.subWord = λ a b → a -64 b
out > Word.mulWord = λ a b → a *64 b
out > Word.NonZero = _
out > Word.div = λ a b _ → quot a b
out > Word.mod = λ a b _ → rem a b
out > Word.NonZeroWord = _
out > Word.divWord = λ a b _ → quot64 a b
out > Word.modWord = λ a b _ → rem64 a b
out > Word.eqWord = λ a b → a ==64 b
out > Word.ltWord = λ a b → a <64 b
out > Word.2^63 = 1 +64 quot64 (0 -64 1) 2
out > Word.test = 100 +64 Word.2^63 +64 (1 +64 Word.2^63)
out > Word.prf = _
out > Word.prf' = _
out > Word.main = Word.putStrLn (Word.showWord Word.test)
out > Word.ltDouble = λ a b → 2 *64 a <64 b
out > Word.lt4x = λ a _ → let b = 2 *64 a in seq b (Word.ltDouble b) b
out > 101
out >
